Nuprl Lemma : es-dt-ap
11,40
postcript
pdf
da
,
l
,
tg
:top. sqequal(fpf-ap(es-dt(
l
;
da
); id-deq;
tg
); fpf-ap(
da
; Kind-deq; rcv(
l
,
tg
)))
latex
Definitions
top
,
t
T
,
x
:
A
.
B
(
x
)
,
compose-fpf(
a
;
b
;
f
)
,
fpf-ap(
f
;
eq
;
x
)
,
es-dt(
l
;
da
)
Lemmas
top
wf
origin
da,l,tg:top. sqequal(fpf-ap(es-dt(l; da); id-deq; tg); fpf-ap(da; Kind-deq; rcv(l,tg))) da,l,tg:top. sqequal(fpf-ap(es-dt(l; da); id-deq; tg); fpf-ap(da; Kind-deq; rcv(l,tg))) 
Tx:A. B(x)